(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
from(X) → cons(X, n__from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, activate(Z)))
2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, activate(Z)))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
activate(n__from(X)) → from(X)
activate(X) → X
Rewrite Strategy: FULL
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
from(X) → cons(X, n__from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, activate(Z)))
2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, activate(Z)))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
activate(n__from(X)) → from(X)
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(3) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
from/0
cons/0
n__from/0
cons2/0
rcons/0
posrecip/0
negrecip/0
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
from → cons(n__from)
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(Z)) → 2ndspos(s(N), cons2(activate(Z)))
2ndspos(s(N), cons2(cons(Z))) → rcons(2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(Z)) → 2ndsneg(s(N), cons2(activate(Z)))
2ndsneg(s(N), cons2(cons(Z))) → rcons(2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from)
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from → n__from
activate(n__from) → from
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(5) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
2ndspos(s(s(N636_1)), cons(cons(cons2(cons(Z637_1))))) →+ rcons(rcons(2ndspos(N636_1, Z637_1)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].
The pumping substitution is [N636_1 / s(s(N636_1)), Z637_1 / cons(cons(cons2(cons(Z637_1))))].
The result substitution is [ ].
(6) BOUNDS(n^1, INF)